<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>Stlc: The Simply Typed Lambda-Calculus</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>
</head>

<body>

<div id="page">

<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 2: Programming Language Foundations</a></div>
<ul id='menu'>
   <li class='section_name'><a href='toc.html'>Table of Contents</a></li>
   <li class='section_name'><a href='coqindex.html'>Index</a></li>
   <li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>

<div id="main">

<h1 class="libtitle">Stlc<span class="subtitle">The Simply Typed Lambda-Calculus</span></h1>

<div class="code">
</div>

<div class="doc">

<div class="paragraph"> </div>

 The simply typed lambda-calculus (STLC) is a tiny core
    calculus embodying the key concept of <i>functional abstraction</i>,
    which shows up in pretty much every real-world programming
    language in some form (functions, procedures, methods, etc.).

<div class="paragraph"> </div>

    We will follow exactly the same pattern as in the previous chapter
    when formalizing this calculus (syntax, small-step semantics,
    typing rules) and its main properties (progress and preservation).
    The new technical challenges arise from the mechanisms of
    <i>variable binding</i> and <i>substitution</i>.  It will take some work to
    deal with these. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Set</span> <span class="id" title="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#"><span class="id" title="library">Strings.String</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">Maps</span>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Smallstep.html#"><span class="id" title="library">Smallstep</span></a>.<br/>
</div>

<div class="doc">
<a id="lab216"></a><h1 class="section">Overview</h1>

<div class="paragraph"> </div>

 The STLC is built on some collection of <i>base types</i>:
    booleans, numbers, strings, etc.  The exact choice of base types
    doesn't matter much -- the construction of the language and its
    theoretical properties work out the same no matter what we
    choose -- so for the sake of brevity let's take just <span class="inlinecode"><span class="id" title="var">Bool</span></span> for
    the moment.  At the end of the chapter we'll see how to add more
    base types, and in later chapters we'll enrich the pure STLC with
    other useful constructs like pairs, records, subtyping, and
    mutable state.

<div class="paragraph"> </div>

    Starting from boolean constants and conditionals, we add three
    things:
<ul class="doclist">
<li> variables

</li>
<li> function abstractions

</li>
<li> application

</li>
</ul>

<div class="paragraph"> </div>

    This gives us the following collection of abstract syntax
    constructors (written out first in informal BNF notation -- we'll
    formalize it below). 
<div class="paragraph"> </div>

<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">t</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" title="var">x</span>                         (<span class="id" title="var">variable</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| \<span class="id" title="var">x</span>:<span class="id" title="var">T</span>,<span class="id" title="var">t</span>                    (<span class="id" title="var">abstraction</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">t</span> <span class="id" title="var">t</span>                       (<span class="id" title="var">application</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">true</span>                      (<span class="id" title="var">constant</span> <span class="id" title="var">true</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">false</span>                     (<span class="id" title="var">constant</span> <span class="id" title="var">false</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="keyword">if</span> <span class="id" title="var">t</span> <span class="id" title="keyword">then</span> <span class="id" title="var">t</span> <span class="id" title="keyword">else</span> <span class="id" title="var">t</span>        (<span class="id" title="var">conditional</span>)
<div class="paragraph"> </div>

</span>
<div class="paragraph"> </div>

 The <span class="inlinecode">\</span> symbol in a function abstraction <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">T</span>,<span class="id" title="var">t</span></span> is generally
    written as a Greek letter "lambda" (hence the name of the
    calculus).  The variable <span class="inlinecode"><span class="id" title="var">x</span></span> is called the <i>parameter</i> to the
    function; the term <span class="inlinecode"><span class="id" title="var">t</span></span> is its <i>body</i>.  The annotation <span class="inlinecode">:<span class="id" title="var">T</span></span>
    specifies the type of arguments that the function can be applied
    to. 
<div class="paragraph"> </div>

 If you've seen lambda-calculus notation before, you might be
    wondering why abstraction is written here as <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">T</span>,<span class="id" title="var">t</span></span> instead of
    the usual "<span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">T.t</span></span>". The reason is that some front ends for
    interacting with Coq use period to separate a file into
    "sentences" to be passed separately to the Coq top level. 
<div class="paragraph"> </div>

 Some examples:

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span></span>

<div class="paragraph"> </div>

        The identity function for booleans.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">(\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span>)</span> <span class="inlinecode"><span class="id" title="var">true</span></span>

<div class="paragraph"> </div>

        The identity function for booleans, applied to the boolean <span class="inlinecode"><span class="id" title="var">true</span></span>.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="keyword">if</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode"><span class="id" title="var">false</span></span> <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode"><span class="id" title="var">true</span></span>

<div class="paragraph"> </div>

        The boolean "not" function.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">true</span></span>

<div class="paragraph"> </div>

        The constant function that takes every (boolean) argument to
        <span class="inlinecode"><span class="id" title="var">true</span></span>. 
</li>
</ul>

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span></span>

<div class="paragraph"> </div>

        A two-argument function that takes two booleans and returns
        the first one.  (As in Coq, a two-argument function is really
        a one-argument function whose body is also a one-argument
        function.)

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">(\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span>)</span> <span class="inlinecode"><span class="id" title="var">false</span></span> <span class="inlinecode"><span class="id" title="var">true</span></span>

<div class="paragraph"> </div>

        A two-argument function that takes two booleans and returns
        the first one, applied to the booleans <span class="inlinecode"><span class="id" title="var">false</span></span> and <span class="inlinecode"><span class="id" title="var">true</span></span>.

<div class="paragraph"> </div>

        As in Coq, application associates to the left -- i.e., this
        expression is parsed as <span class="inlinecode">((\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span>)</span> <span class="inlinecode"><span class="id" title="var">false</span>)</span> <span class="inlinecode"><span class="id" title="var">true</span></span>.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">\<span class="id" title="var">f</span>:<span class="id" title="var">Bool</span>→<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">f</span></span> <span class="inlinecode">(<span class="id" title="var">f</span></span> <span class="inlinecode"><span class="id" title="var">true</span>)</span>

<div class="paragraph"> </div>

        A higher-order function that takes a <i>function</i> <span class="inlinecode"><span class="id" title="var">f</span></span> (from
        booleans to booleans) as an argument, applies <span class="inlinecode"><span class="id" title="var">f</span></span> to <span class="inlinecode"><span class="id" title="var">true</span></span>,
        and applies <span class="inlinecode"><span class="id" title="var">f</span></span> again to the result.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">(\<span class="id" title="var">f</span>:<span class="id" title="var">Bool</span>→<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">f</span></span> <span class="inlinecode">(<span class="id" title="var">f</span></span> <span class="inlinecode"><span class="id" title="var">true</span>))</span> <span class="inlinecode">(\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">false</span>)</span>

<div class="paragraph"> </div>

        The same higher-order function, applied to the constantly
        <span class="inlinecode"><span class="id" title="var">false</span></span> function. 
</li>
</ul>

<div class="paragraph"> </div>

 As the last several examples show, the STLC is a language of
    <i>higher-order</i> functions: we can write down functions that take
    other functions as arguments and/or return other functions as
    results.

<div class="paragraph"> </div>

    The STLC doesn't provide any primitive syntax for defining <i>named</i>
    functions -- all functions are "anonymous."  We'll see in chapter
    <span class="inlinecode"><span class="id" title="var">MoreStlc</span></span> that it is easy to add named functions to what we've
    got -- indeed, the fundamental naming and binding mechanisms are
    exactly the same.

<div class="paragraph"> </div>

    The <i>types</i> of the STLC include <span class="inlinecode"><span class="id" title="var">Bool</span></span>, which classifies the
    boolean constants <span class="inlinecode"><span class="id" title="var">true</span></span> and <span class="inlinecode"><span class="id" title="var">false</span></span> as well as more complex
    computations that yield booleans, plus <i>arrow types</i> that classify
    functions. 
<div class="paragraph"> </div>

<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">T</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" title="var">Bool</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">T</span> → <span class="id" title="var">T</span>
<div class="paragraph"> </div>

</span>    For example:

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">false</span></span> has type <span class="inlinecode"><span class="id" title="var">Bool</span>→<span class="id" title="var">Bool</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span></span> has type <span class="inlinecode"><span class="id" title="var">Bool</span>→<span class="id" title="var">Bool</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">(\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span>)</span> <span class="inlinecode"><span class="id" title="var">true</span></span> has type <span class="inlinecode"><span class="id" title="var">Bool</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span></span> has type <span class="inlinecode"><span class="id" title="var">Bool</span>→<span class="id" title="var">Bool</span>→<span class="id" title="var">Bool</span></span>
                              (i.e., <span class="inlinecode"><span class="id" title="var">Bool</span></span> <span class="inlinecode">→</span> <span class="inlinecode">(<span class="id" title="var">Bool</span>→<span class="id" title="var">Bool</span>)</span>)

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">(\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span>)</span> <span class="inlinecode"><span class="id" title="var">false</span></span> has type <span class="inlinecode"><span class="id" title="var">Bool</span>→<span class="id" title="var">Bool</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">(\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span>)</span> <span class="inlinecode"><span class="id" title="var">false</span></span> <span class="inlinecode"><span class="id" title="var">true</span></span> has type <span class="inlinecode"><span class="id" title="var">Bool</span></span> 
</li>
</ul>

</div>

<div class="doc">
<a id="lab217"></a><h1 class="section">Syntax</h1>

<div class="paragraph"> </div>

 We next formalize the syntax of the STLC. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Module</span> <a id="STLC" class="idref" href="#STLC"><span class="id" title="module">STLC</span></a>.<br/>
</div>

<div class="doc">
<a id="lab218"></a><h2 class="section">Types</h2>

</div>
<div class="code">

<br/>
<span class="id" title="keyword">Inductive</span> <a id="STLC.ty" class="idref" href="#STLC.ty"><span class="id" title="inductive">ty</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="STLC.Ty_Bool" class="idref" href="#STLC.Ty_Bool"><span class="id" title="constructor">Ty_Bool</span></a>  : <a class="idref" href="Stlc.html#ty:1"><span class="id" title="inductive">ty</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.Ty_Arrow" class="idref" href="#STLC.Ty_Arrow"><span class="id" title="constructor">Ty_Arrow</span></a> : <a class="idref" href="Stlc.html#ty:1"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#ty:1"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#ty:1"><span class="id" title="inductive">ty</span></a>.<br/>
</div>

<div class="doc">
<a id="lab219"></a><h2 class="section">Terms</h2>

</div>
<div class="code">

<br/>
<span class="id" title="keyword">Inductive</span> <a id="STLC.tm" class="idref" href="#STLC.tm"><span class="id" title="inductive">tm</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="STLC.tm_var" class="idref" href="#STLC.tm_var"><span class="id" title="constructor">tm_var</span></a>   : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.tm_app" class="idref" href="#STLC.tm_app"><span class="id" title="constructor">tm_app</span></a>   : <a class="idref" href="Stlc.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.tm_abs" class="idref" href="#STLC.tm_abs"><span class="id" title="constructor">tm_abs</span></a>   : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#STLC.ty"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.tm_true" class="idref" href="#STLC.tm_true"><span class="id" title="constructor">tm_true</span></a>  : <a class="idref" href="Stlc.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.tm_false" class="idref" href="#STLC.tm_false"><span class="id" title="constructor">tm_false</span></a> : <a class="idref" href="Stlc.html#tm:3"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.tm_if" class="idref" href="#STLC.tm_if"><span class="id" title="constructor">tm_if</span></a>    : <a class="idref" href="Stlc.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#tm:3"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#tm:3"><span class="id" title="inductive">tm</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="var">Declare</span> <span class="id" title="var">Custom</span> <span class="id" title="var">Entry</span> <span class="id" title="var">stlc</span>.<br/>
<span class="id" title="keyword">Notation</span> <a id="eaa77420ac6a1aef5b440889c7543807" class="idref" href="#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&quot;</span></a>&lt;{ e }&gt;" := <span class="id" title="var">e</span> (<span class="id" title="var">e</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99).<br/>
<span class="id" title="keyword">Notation</span> <a id="356f9b00d0ca8b465f5c07428196b78a" class="idref" href="#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">&quot;</span></a>( x )" := <span class="id" title="var">x</span> (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span>, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLC.:stlc::x" class="idref" href="#STLC.:stlc::x"><span class="id" title="notation">&quot;</span></a>x" := <span class="id" title="var">x</span> (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="keyword">constr</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLC.:stlc::x_'-&gt;'_x" class="idref" href="#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">&quot;</span></a>S <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> T" := (<a class="idref" href="Stlc.html#STLC.Ty_Arrow"><span class="id" title="constructor">Ty_Arrow</span></a> <span class="id" title="var">S</span> <span class="id" title="var">T</span>) (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 50, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLC.:stlc::x_x" class="idref" href="#STLC.:stlc::x_x"><span class="id" title="notation">&quot;</span></a>x y" := (<a class="idref" href="Stlc.html#STLC.tm_app"><span class="id" title="constructor">tm_app</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 1, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="28c1f0fbf2e9b1fd5a138d34ed0aa145" class="idref" href="#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">&quot;</span></a>\ x : t , y" :=<br/>
&nbsp;&nbsp;(<a class="idref" href="Stlc.html#STLC.tm_abs"><span class="id" title="constructor">tm_abs</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> <span class="id" title="var">y</span>) (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 90, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">t</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">y</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Coercion</span> <a class="idref" href="Stlc.html#STLC.tm_var"><span class="id" title="constructor">tm_var</span></a> <a class="idref" href="Stlc.html#STLC.tm_var"><span class="id" title="constructor">:</span></a> <a class="idref" href="Stlc.html#STLC.tm_var"><span class="id" title="constructor">string</span></a> <a class="idref" href="Stlc.html#STLC.tm_var"><span class="id" title="constructor">&gt;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Stlc.html#STLC.tm_var"><span class="id" title="constructor">tm</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLC.:stlc::'Bool'" class="idref" href="#STLC.:stlc::'Bool'"><span class="id" title="notation">&quot;</span></a>'Bool'" := <a class="idref" href="Stlc.html#STLC.Ty_Bool"><span class="id" title="constructor">Ty_Bool</span></a> (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLC.:stlc::'if'_x_'then'_x_'else'_x" class="idref" href="#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">&quot;</span></a>'if' x 'then' y 'else' z" :=<br/>
&nbsp;&nbsp;(<a class="idref" href="Stlc.html#STLC.tm_if"><span class="id" title="constructor">tm_if</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span>) (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 89,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">x</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">y</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">z</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLC.:::'true'" class="idref" href="#STLC.:::'true'"><span class="id" title="notation">&quot;</span></a>'true'"  := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 1).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLC.:stlc::'true'" class="idref" href="#STLC.:stlc::'true'"><span class="id" title="notation">&quot;</span></a>'true'"  := <a class="idref" href="Stlc.html#STLC.tm_true"><span class="id" title="constructor">tm_true</span></a> (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLC.:::'false'" class="idref" href="#STLC.:::'false'"><span class="id" title="notation">&quot;</span></a>'false'"  := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 1).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLC.:stlc::'false'" class="idref" href="#STLC.:stlc::'false'"><span class="id" title="notation">&quot;</span></a>'false'"  := <a class="idref" href="Stlc.html#STLC.tm_false"><span class="id" title="constructor">tm_false</span></a> (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
</div>

<div class="doc">
Some more notation magic to set up the concrete syntax, as we did
    in the <span class="inlinecode"><span class="id" title="var">Imp</span></span> chapter... 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Definition</span> <a id="STLC.x" class="idref" href="#STLC.x"><span class="id" title="definition">x</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> := "x".<br/>
<span class="id" title="keyword">Definition</span> <a id="STLC.y" class="idref" href="#STLC.y"><span class="id" title="definition">y</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> := "y".<br/>
<span class="id" title="keyword">Definition</span> <a id="STLC.z" class="idref" href="#STLC.z"><span class="id" title="definition">z</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> := "z".<br/>
<span class="id" title="keyword">Hint Unfold</span> <a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a> : <span class="id" title="var">core</span>.<br/>
<span class="id" title="keyword">Hint Unfold</span> <a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a> : <span class="id" title="var">core</span>.<br/>
<span class="id" title="keyword">Hint Unfold</span> <a class="idref" href="Stlc.html#STLC.z"><span class="id" title="definition">z</span></a> : <span class="id" title="var">core</span>.<br/>
</div>

<div class="doc">
Note that an abstraction <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">T</span>,<span class="id" title="var">t</span></span> (formally, <span class="inlinecode"><span class="id" title="var">tm_abs</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span>) is
    always annotated with the type <span class="inlinecode"><span class="id" title="var">T</span></span> of its parameter, in contrast
    to Coq (and other functional languages like ML, Haskell, etc.),
    which use type inference to fill in missing annotations.  We're
    not considering type inference here. 
<div class="paragraph"> </div>

 Some examples... 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Notation</span> <a id="STLC.idB" class="idref" href="#STLC.idB"><span class="id" title="abbreviation">idB</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLC.idBB" class="idref" href="#STLC.idBB"><span class="id" title="abbreviation">idBB</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLC.idBBBB" class="idref" href="#STLC.idBBBB"><span class="id" title="abbreviation">idBBBB</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">((</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">))</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLC.k" class="idref" href="#STLC.k"><span class="id" title="abbreviation">k</span></a> := <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLC.notB" class="idref" href="#STLC.notB"><span class="id" title="abbreviation">notB</span></a> := <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'false'"><span class="id" title="notation">false</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>.<br/>
</div>

<div class="doc">
(We write these as <span class="inlinecode"><span class="id" title="keyword">Notation</span></span>s rather than <span class="inlinecode"><span class="id" title="keyword">Definition</span></span>s to make
    things easier for <span class="inlinecode"><span class="id" title="tactic">auto</span></span>.) 
</div>

<div class="doc">
<a id="lab220"></a><h1 class="section">Operational Semantics</h1>

<div class="paragraph"> </div>

 To define the small-step semantics of STLC terms, we begin,
    as always, by defining the set of values.  Next, we define the
    critical notions of <i>free variables</i> and <i>substitution</i>, which are
    used in the reduction rule for application expressions.  And
    finally we give the small-step relation itself. 
</div>

<div class="doc">
<a id="lab221"></a><h2 class="section">Values</h2>

<div class="paragraph"> </div>

 To define the values of the STLC, we have a few cases to consider.

<div class="paragraph"> </div>

    First, for the boolean part of the language, the situation is
    clear: <span class="inlinecode"><span class="id" title="var">true</span></span> and <span class="inlinecode"><span class="id" title="var">false</span></span> are the only values.  An <span class="inlinecode"><span class="id" title="keyword">if</span></span> expression
    is never a value. 
<div class="paragraph"> </div>

 Second, an application is not a value: it represents a function
    being invoked on some argument, which clearly still has work left
    to do. 
<div class="paragraph"> </div>

 Third, for abstractions, we have a choice:

<div class="paragraph"> </div>

<ul class="doclist">
<li> We can say that <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">T</span>,</span> <span class="inlinecode"><span class="id" title="var">t</span></span> is a value only when <span class="inlinecode"><span class="id" title="var">t</span></span> is a
        value -- i.e., only if the function's body has been
        reduced (as much as it can be without knowing what argument it
        is going to be applied to).

<div class="paragraph"> </div>


</li>
<li> Or we can say that <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">T</span>,</span> <span class="inlinecode"><span class="id" title="var">t</span></span> is always a value, no matter
        whether <span class="inlinecode"><span class="id" title="var">t</span></span> is one or not -- in other words, we can say that
        reduction stops at abstractions.

</li>
</ul>

<div class="paragraph"> </div>

    Our usual way of evaluating expressions in Gallina makes the first
    choice -- for example,
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Compute</span> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span>:<span class="id" title="var">bool</span> ⇒ 3 + 4)
<div class="paragraph"> </div>

</span>    yields:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span>:<span class="id" title="var">bool</span> ⇒ 7
<div class="paragraph"> </div>

</span>    Most real-world functional programming languages make the second
    choice -- reduction of a function's body only begins when the
    function is actually applied to an argument.  We also make the
    second choice here. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Inductive</span> <a id="STLC.value" class="idref" href="#STLC.value"><span class="id" title="inductive">value</span></a> : <a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="STLC.v_abs" class="idref" href="#STLC.v_abs"><span class="id" title="constructor">v_abs</span></a> : <span class="id" title="keyword">∀</span> <a id="x:7" class="idref" href="#x:7"><span class="id" title="binder">x</span></a> <a id="T<sub>2</sub>:8" class="idref" href="#T<sub>2</sub>:8"><span class="id" title="binder">T<sub>2</sub></span></a> <a id="t<sub>1</sub>:9" class="idref" href="#t<sub>1</sub>:9"><span class="id" title="binder">t<sub>1</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#value:5"><span class="id" title="inductive">value</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#x:7"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#T<sub>2</sub>:8"><span class="id" title="variable">T<sub>2</sub></span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>:9"><span class="id" title="variable">t<sub>1</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.v_true" class="idref" href="#STLC.v_true"><span class="id" title="constructor">v_true</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#value:5"><span class="id" title="inductive">value</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.v_false" class="idref" href="#STLC.v_false"><span class="id" title="constructor">v_false</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#value:5"><span class="id" title="inductive">value</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'false'"><span class="id" title="notation">false</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="Stlc.html#value"><span class="id" title="inductive">value</span></a> : <span class="id" title="var">core</span>.<br/>
</div>

<div class="doc">
Finally, we must consider what constitutes a <i>complete</i> program.

<div class="paragraph"> </div>

    Intuitively, a "complete program" must not refer to any undefined
    variables.  We'll see shortly how to define the <i>free</i> variables
    in a STLC term.  A complete program is <i>closed</i> -- that is, it
    contains no free variables.

<div class="paragraph"> </div>

    (Conversely, a term with free variables is often called an <i>open
    term</i>.) 
<div class="paragraph"> </div>

 Having made the choice not to reduce under abstractions, we don't
    need to worry about whether variables are values, since we'll
    always be reducing programs "from the outside in," and that means
    the <span class="inlinecode"><span class="id" title="var">step</span></span> relation will always be working with closed terms.  
</div>

<div class="doc">
<a id="lab222"></a><h2 class="section">Substitution</h2>

<div class="paragraph"> </div>

 Now we come to the heart of the STLC: the operation of
    substituting one term for a variable in another term.  This
    operation is used below to define the operational semantics of
    function application, where we will need to substitute the
    argument term for the function parameter in the function's body.
    For example, we reduce
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>, <span class="id" title="keyword">if</span> <span class="id" title="var">x</span> <span class="id" title="keyword">then</span> <span class="id" title="var">true</span> <span class="id" title="keyword">else</span> <span class="id" title="var">x</span>) <span class="id" title="var">false</span>
<div class="paragraph"> </div>

</span>    to
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <span class="id" title="var">false</span> <span class="id" title="keyword">then</span> <span class="id" title="var">true</span> <span class="id" title="keyword">else</span> <span class="id" title="var">false</span>
<div class="paragraph"> </div>

</span>    by substituting <span class="inlinecode"><span class="id" title="var">false</span></span> for the parameter <span class="inlinecode"><span class="id" title="var">x</span></span> in the body of the
    function.

<div class="paragraph"> </div>

    In general, we need to be able to substitute some given term <span class="inlinecode"><span class="id" title="var">s</span></span>
    for occurrences of some variable <span class="inlinecode"><span class="id" title="var">x</span></span> in another term <span class="inlinecode"><span class="id" title="var">t</span></span>.  In
    informal discussions, this is usually written <span class="inlinecode"></span> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>]<span class="id" title="var">t</span></span> <span class="inlinecode"></span> and
    pronounced "substitute <span class="inlinecode"><span class="id" title="var">s</span></span> for <span class="inlinecode"><span class="id" title="var">x</span></span> in <span class="inlinecode"><span class="id" title="var">t</span></span>." 
<div class="paragraph"> </div>

 Here are some examples:

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">true</span>]</span> <span class="inlinecode">(<span class="id" title="keyword">if</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode"><span class="id" title="var">false</span>)</span>
           yields <span class="inlinecode"><span class="id" title="keyword">if</span></span> <span class="inlinecode"><span class="id" title="var">true</span></span> <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode"><span class="id" title="var">true</span></span> <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode"><span class="id" title="var">false</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">true</span>]</span> <span class="inlinecode"><span class="id" title="var">x</span></span> yields <span class="inlinecode"><span class="id" title="var">true</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">true</span>]</span> <span class="inlinecode">(<span class="id" title="keyword">if</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode"><span class="id" title="var">y</span>)</span> yields <span class="inlinecode"><span class="id" title="keyword">if</span></span> <span class="inlinecode"><span class="id" title="var">true</span></span> <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode"><span class="id" title="var">true</span></span> <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">true</span>]</span> <span class="inlinecode"><span class="id" title="var">y</span></span> yields <span class="inlinecode"><span class="id" title="var">y</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">true</span>]</span> <span class="inlinecode"><span class="id" title="var">false</span></span> yields <span class="inlinecode"><span class="id" title="var">false</span></span> (vacuous substitution)

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">true</span>]</span> <span class="inlinecode">(\<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="keyword">if</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span> <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode"><span class="id" title="var">false</span>)</span>
           yields <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="keyword">if</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span> <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode"><span class="id" title="var">true</span></span> <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode"><span class="id" title="var">false</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">true</span>]</span> <span class="inlinecode">(\<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span>)</span> yields <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">true</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">true</span>]</span> <span class="inlinecode">(\<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">y</span>)</span> yields <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">y</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">true</span>]</span> <span class="inlinecode">(\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span>)</span> yields <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span></span>

</li>
</ul>

<div class="paragraph"> </div>

    The last example is very important: substituting <span class="inlinecode"><span class="id" title="var">x</span></span> with <span class="inlinecode"><span class="id" title="var">true</span></span> in
    <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span></span> does <i>not</i> yield <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">true</span></span>!  The reason for
    this is that the <span class="inlinecode"><span class="id" title="var">x</span></span> in the body of <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span></span> is <i>bound</i> by the
    abstraction: it is a new, local name that just happens to be
    spelled the same as some global name <span class="inlinecode"><span class="id" title="var">x</span></span>. 
<div class="paragraph"> </div>

 Here is the definition, informally...
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>]<span class="id" title="var">x</span>               = <span class="id" title="var">s</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>]<span class="id" title="var">y</span>               = <span class="id" title="var">y</span>                     <span class="id" title="keyword">if</span> <span class="id" title="var">x</span> ≠ <span class="id" title="var">y</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>](\<span class="id" title="var">x</span>:<span class="id" title="var">T</span>, <span class="id" title="var">t</span>)       = \<span class="id" title="var">x</span>:<span class="id" title="var">T</span>, <span class="id" title="var">t</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>](\<span class="id" title="var">y</span>:<span class="id" title="var">T</span>, <span class="id" title="var">t</span>)       = \<span class="id" title="var">y</span>:<span class="id" title="var">T</span>, [<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>]<span class="id" title="var">t</span>         <span class="id" title="keyword">if</span> <span class="id" title="var">x</span> ≠ <span class="id" title="var">y</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>](<span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span>)         = ([<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>]<span class="id" title="var">t<sub>1</sub></span>) ([<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>]<span class="id" title="var">t<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>]<span class="id" title="var">true</span>            = <span class="id" title="var">true</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>]<span class="id" title="var">false</span>           = <span class="id" title="var">false</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>](<span class="id" title="keyword">if</span> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="keyword">then</span> <span class="id" title="var">t<sub>2</sub></span> <span class="id" title="keyword">else</span> <span class="id" title="var">t<sub>3</sub></span>) =<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> [<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>]<span class="id" title="var">t<sub>1</sub></span> <span class="id" title="keyword">then</span> [<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>]<span class="id" title="var">t<sub>2</sub></span> <span class="id" title="keyword">else</span> [<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>]<span class="id" title="var">t<sub>3</sub></span>
<div class="paragraph"> </div>

</span>
<div class="paragraph"> </div>

 ... and formally: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Reserved Notation</span> &quot;'[' x ':=' s ']' t" (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 20, <span class="id" title="var">x</span> <span class="id" title="keyword">constr</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="STLC.subst" class="idref" href="#STLC.subst"><span class="id" title="definition">subst</span></a> (<a id="x:10" class="idref" href="#x:10"><span class="id" title="binder">x</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) (<a id="s:11" class="idref" href="#s:11"><span class="id" title="binder">s</span></a> : <a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a>) (<a id="t:12" class="idref" href="#t:12"><span class="id" title="binder">t</span></a> : <a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a>) : <a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Stlc.html#t:12"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#STLC.tm_var"><span class="id" title="constructor">tm_var</span></a> <span class="id" title="var">y</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <span class="id" title="definition">eqb_string</span> <a class="idref" href="Stlc.html#x:10"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span> <span class="id" title="keyword">then</span> <a class="idref" href="Stlc.html#s:11"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="Stlc.html#t:12"><span class="id" title="variable">t</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><span class="id" title="var">y</span><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><span class="id" title="var">T</span><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <span class="id" title="definition">eqb_string</span> <a class="idref" href="Stlc.html#x:10"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span> <span class="id" title="keyword">then</span> <a class="idref" href="Stlc.html#t:12"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><span class="id" title="var">y</span><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><span class="id" title="var">T</span><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">[</span></a><a class="idref" href="Stlc.html#x:10"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">:=</span></a><a class="idref" href="Stlc.html#s:11"><span class="id" title="variable">s</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">[</span></a><a class="idref" href="Stlc.html#x:10"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">:=</span></a><a class="idref" href="Stlc.html#s:11"><span class="id" title="variable">s</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">[</span></a><a class="idref" href="Stlc.html#x:10"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">:=</span></a><a class="idref" href="Stlc.html#s:11"><span class="id" title="variable">s</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'false'"><span class="id" title="notation">false</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'false'"><span class="id" title="notation">false</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <span class="id" title="var">t<sub>3</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">[</span></a><a class="idref" href="Stlc.html#x:10"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">:=</span></a><a class="idref" href="Stlc.html#s:11"><span class="id" title="variable">s</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">[</span></a><a class="idref" href="Stlc.html#x:10"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">:=</span></a><a class="idref" href="Stlc.html#s:11"><span class="id" title="variable">s</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">[</span></a><a class="idref" href="Stlc.html#x:10"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">:=</span></a><a class="idref" href="Stlc.html#s:11"><span class="id" title="variable">s</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>3</sub></span><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
<br/>
<span class="id" title="keyword">where</span> <a id="af81635d67c091f2566d9a89993ee012" class="idref" href="#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">&quot;</span></a>'[' x ':=' s ']' t" := (<a class="idref" href="Stlc.html#subst:13"><span class="id" title="definition">subst</span></a> <span class="id" title="var">x</span> <span class="id" title="var">s</span> <span class="id" title="var">t</span>) (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span>).<br/>
</div>

<div class="doc">
Note on notations: You might be wondering why we need curly braces
    around the substitution notation in the above definition, and why
    do we need to redefine the substition notation in the <span class="inlinecode"><span class="id" title="var">stlc</span></span>
    custom grammar. The reason is that reserved notations in
    definitions have to be defined in the general Coq grammar (and not
    a custom one like <span class="inlinecode"><span class="id" title="var">stlc</span></span>). This restriction only applies to the
    <span class="inlinecode"><span class="id" title="tactic">subst</span></span> definition, that is before the <span class="inlinecode"><span class="id" title="keyword">where</span></span> <span class="inlinecode">...</span> part. From now
    on, using the substitution notation in the <span class="inlinecode"><span class="id" title="var">stlc</span></span> custom grammar
    doesn't need any curly braces. 
<div class="paragraph"> </div>

 For example... 
</div>
<div class="code">
<span class="id" title="keyword">Check</span> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">[</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">:=</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">]</span></a> <a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>.<br/>
</div>

<div class="doc">
<i>Technical note</i>: Substitution becomes trickier to define if we
    consider the case where <span class="inlinecode"><span class="id" title="var">s</span></span>, the term being substituted for a
    variable in some other term, may itself contain free variables. 
    Since we are only interested here in defining the <span class="inlinecode"><span class="id" title="var">step</span></span> relation
    on <i>closed</i> terms (i.e., terms like <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span></span> that include
    binders for all of the variables they mention), we can sidestep this
    extra complexity, but it must be dealt with when formalizing
    richer languages. 
<div class="paragraph"> </div>

 For example, using the definition of substitution above to
    substitute the <i>open</i> term <span class="inlinecode"><span class="id" title="var">s</span></span> <span class="inlinecode">=</span> <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">r</span></span>, where <span class="inlinecode"><span class="id" title="var">r</span></span> is a <i>free</i>
    reference to some global resource, for the variable <span class="inlinecode"><span class="id" title="var">z</span></span> in the
    term <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode">\<span class="id" title="var">r</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">z</span></span>, where <span class="inlinecode"><span class="id" title="var">r</span></span> is a bound variable, we would get
    <span class="inlinecode">\<span class="id" title="var">r</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">r</span></span>, where the free reference to <span class="inlinecode"><span class="id" title="var">r</span></span> in <span class="inlinecode"><span class="id" title="var">s</span></span> has
    been "captured" by the binder at the beginning of <span class="inlinecode"><span class="id" title="var">t</span></span>.

<div class="paragraph"> </div>

    Why would this be bad?  Because it violates the principle that the
    names of bound variables do not matter.  For example, if we rename
    the bound variable in <span class="inlinecode"><span class="id" title="var">t</span></span>, e.g., let <span class="inlinecode"><span class="id" title="var">t'</span></span> <span class="inlinecode">=</span> <span class="inlinecode">\<span class="id" title="var">w</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">z</span></span>, then
    <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>]<span class="id" title="var">t'</span></span> is <span class="inlinecode">\<span class="id" title="var">w</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">r</span></span>, which does not behave the
    same as <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">s</span>]<span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode">\<span class="id" title="var">r</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">r</span></span>.  That is, renaming a
    bound variable changes how <span class="inlinecode"><span class="id" title="var">t</span></span> behaves under substitution. 
<div class="paragraph"> </div>

 See, for example, <a href="Bib.html#Aydemir-2008"><span class="inlineref">[Aydemir 2008]</span></a> for further discussion
    of this issue. 
<div class="paragraph"> </div>

<a id="lab223"></a><h4 class="section">Exercise: 3 stars, standard (substi_correct)</h4>
 The definition that we gave above uses Coq's <span class="inlinecode"><span class="id" title="keyword">Fixpoint</span></span> facility
    to define substitution as a <i>function</i>.  Suppose, instead, we
    wanted to define substitution as an inductive <i>relation</i> <span class="inlinecode"><span class="id" title="var">substi</span></span>.
    We've begun the definition by providing the <span class="inlinecode"><span class="id" title="keyword">Inductive</span></span> header and
    one of the construectors; your job is to fill in the rest of the
    constructors and prove that the relation you've defined coincides
    with the function given above. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Inductive</span> <a id="STLC.substi" class="idref" href="#STLC.substi"><span class="id" title="inductive">substi</span></a> (<a id="s:15" class="idref" href="#s:15"><span class="id" title="binder">s</span></a> : <a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a>) (<a id="x:16" class="idref" href="#x:16"><span class="id" title="binder">x</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="STLC.s_var1" class="idref" href="#STLC.s_var1"><span class="id" title="constructor">s_var1</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#substi:17"><span class="id" title="inductive">substi</span></a> <a class="idref" href="Stlc.html#s:15"><span class="id" title="variable">s</span></a> <a class="idref" href="Stlc.html#x:16"><span class="id" title="variable">x</span></a> (<a class="idref" href="Stlc.html#STLC.tm_var"><span class="id" title="constructor">tm_var</span></a> <a class="idref" href="Stlc.html#x:16"><span class="id" title="variable">x</span></a>) <a class="idref" href="Stlc.html#s:15"><span class="id" title="variable">s</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="Stlc.html#substi"><span class="id" title="inductive">substi</span></a> : <span class="id" title="var">core</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="STLC.substi_correct" class="idref" href="#STLC.substi_correct"><span class="id" title="lemma">substi_correct</span></a> : <span class="id" title="keyword">∀</span> <a id="s:19" class="idref" href="#s:19"><span class="id" title="binder">s</span></a> <a id="x:20" class="idref" href="#x:20"><span class="id" title="binder">x</span></a> <a id="t:21" class="idref" href="#t:21"><span class="id" title="binder">t</span></a> <a id="t':22" class="idref" href="#t':22"><span class="id" title="binder">t'</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">[</span></a><a class="idref" href="Stlc.html#x:20"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">:=</span></a><a class="idref" href="Stlc.html#s:19"><span class="id" title="variable">s</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">]</span></a><a class="idref" href="Stlc.html#t:21"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Stlc.html#t':22"><span class="id" title="variable">t'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'&lt;-&gt;'_x"><span class="id" title="notation">↔</span></a> <a class="idref" href="Stlc.html#STLC.substi"><span class="id" title="inductive">substi</span></a> <a class="idref" href="Stlc.html#s:19"><span class="id" title="variable">s</span></a> <a class="idref" href="Stlc.html#x:20"><span class="id" title="variable">x</span></a> <a class="idref" href="Stlc.html#t:21"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#t':22"><span class="id" title="variable">t'</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab224"></a><h2 class="section">Reduction</h2>

<div class="paragraph"> </div>

 The small-step reduction relation for STLC now follows the
    same pattern as the ones we have seen before.  Intuitively, to
    reduce a function application, we first reduce its left-hand
    side (the function) until it becomes an abstraction; then we
    reduce its right-hand side (the argument) until it is also a
    value; and finally we substitute the argument for the bound
    variable in the body of the abstraction.  This last rule, written
    informally as
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(\<span class="id" title="var">x</span>:<span class="id" title="var">T</span>,<span class="id" title="var">t<sub>12</sub></span>) <span class="id" title="var">v<sub>2</sub></span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [<span class="id" title="var">x</span>:=<span class="id" title="var">v<sub>2</sub></span>]<span class="id" title="var">t<sub>12</sub></span>
<div class="paragraph"> </div>

</span>    is traditionally called <i>beta-reduction</i>. 
<div class="paragraph"> </div>

 <center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">value v<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (ST_AppAbs) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">(\x:T<sub>2</sub>,t<sub>1</sub>) v<sub>2</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [x:=v<sub>2</sub>]t<sub>1</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">t<sub>1</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> t<sub>1</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_App1) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">t<sub>1</sub> t<sub>2</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> t<sub>1</sub>' t<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">value v<sub>1</sub></td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">t<sub>2</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> t<sub>2</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_App2) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">v<sub>1</sub> t<sub>2</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> v<sub>1</sub> t<sub>2</sub>'</td>
  <td></td>
</td>
</table></center> ... plus the usual rules for conditionals:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_IfTrue) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">(if true then t<sub>1</sub> else t<sub>2</sub>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> t<sub>1</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_IfFalse) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">(if false then t<sub>1</sub> else t<sub>2</sub>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> t<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">t<sub>1</sub> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> t<sub>1</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_If) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">(if t<sub>1</sub> then t<sub>2</sub> else t<sub>3</sub>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (if t<sub>1</sub>' then t<sub>2</sub> else t<sub>3</sub>)</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

 Formally: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Reserved Notation</span> &quot;t '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>' t'" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Inductive</span> <a id="STLC.step" class="idref" href="#STLC.step"><span class="id" title="inductive">step</span></a> : <a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="STLC.ST_AppAbs" class="idref" href="#STLC.ST_AppAbs"><span class="id" title="constructor">ST_AppAbs</span></a> : <span class="id" title="keyword">∀</span> <a id="x:25" class="idref" href="#x:25"><span class="id" title="binder">x</span></a> <a id="T<sub>2</sub>:26" class="idref" href="#T<sub>2</sub>:26"><span class="id" title="binder">T<sub>2</sub></span></a> <a id="t<sub>1</sub>:27" class="idref" href="#t<sub>1</sub>:27"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="v<sub>2</sub>:28" class="idref" href="#v<sub>2</sub>:28"><span class="id" title="binder">v<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#STLC.value"><span class="id" title="inductive">value</span></a> <a class="idref" href="Stlc.html#v<sub>2</sub>:28"><span class="id" title="variable">v<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#x:25"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#T<sub>2</sub>:26"><span class="id" title="variable">T<sub>2</sub></span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>:27"><span class="id" title="variable">t<sub>1</sub></span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a> <a class="idref" href="Stlc.html#v<sub>2</sub>:28"><span class="id" title="variable">v<sub>2</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#STLC.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">[</span></a><a class="idref" href="Stlc.html#x:25"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">:=</span></a><a class="idref" href="Stlc.html#v<sub>2</sub>:28"><span class="id" title="variable">v<sub>2</sub></span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">]</span></a><a class="idref" href="Stlc.html#t<sub>1</sub>:27"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.ST_App1" class="idref" href="#STLC.ST_App1"><span class="id" title="constructor">ST_App1</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:29" class="idref" href="#t<sub>1</sub>:29"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>1</sub>':30" class="idref" href="#t<sub>1</sub>':30"><span class="id" title="binder">t<sub>1</sub>'</span></a> <a id="t<sub>2</sub>:31" class="idref" href="#t<sub>2</sub>:31"><span class="id" title="binder">t<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#t<sub>1</sub>:29"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#STLC.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>':30"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#t<sub>1</sub>:29"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#t<sub>2</sub>:31"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#STLC.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#t<sub>1</sub>':30"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="Stlc.html#t<sub>2</sub>:31"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.ST_App2" class="idref" href="#STLC.ST_App2"><span class="id" title="constructor">ST_App2</span></a> : <span class="id" title="keyword">∀</span> <a id="v<sub>1</sub>:32" class="idref" href="#v<sub>1</sub>:32"><span class="id" title="binder">v<sub>1</sub></span></a> <a id="t<sub>2</sub>:33" class="idref" href="#t<sub>2</sub>:33"><span class="id" title="binder">t<sub>2</sub></span></a> <a id="t<sub>2</sub>':34" class="idref" href="#t<sub>2</sub>':34"><span class="id" title="binder">t<sub>2</sub>'</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#STLC.value"><span class="id" title="inductive">value</span></a> <a class="idref" href="Stlc.html#v<sub>1</sub>:32"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#t<sub>2</sub>:33"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Stlc.html#STLC.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Stlc.html#t<sub>2</sub>':34"><span class="id" title="variable">t<sub>2</sub>'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#v<sub>1</sub>:32"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="Stlc.html#t<sub>2</sub>:33"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#STLC.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#v<sub>1</sub>:32"><span class="id" title="variable">v<sub>1</sub></span></a>  <a class="idref" href="Stlc.html#t<sub>2</sub>':34"><span class="id" title="variable">t<sub>2</sub>'</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.ST_IfTrue" class="idref" href="#STLC.ST_IfTrue"><span class="id" title="constructor">ST_IfTrue</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:35" class="idref" href="#t<sub>1</sub>:35"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:36" class="idref" href="#t<sub>2</sub>:36"><span class="id" title="binder">t<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>:35"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <a class="idref" href="Stlc.html#t<sub>2</sub>:36"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#STLC.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>:35"><span class="id" title="variable">t<sub>1</sub></span></a><br/>
&nbsp;&nbsp;| <a id="STLC.ST_IfFalse" class="idref" href="#STLC.ST_IfFalse"><span class="id" title="constructor">ST_IfFalse</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:37" class="idref" href="#t<sub>1</sub>:37"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:38" class="idref" href="#t<sub>2</sub>:38"><span class="id" title="binder">t<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'false'"><span class="id" title="notation">false</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>:37"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <a class="idref" href="Stlc.html#t<sub>2</sub>:38"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#STLC.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Stlc.html#t<sub>2</sub>:38"><span class="id" title="variable">t<sub>2</sub></span></a><br/>
&nbsp;&nbsp;| <a id="STLC.ST_If" class="idref" href="#STLC.ST_If"><span class="id" title="constructor">ST_If</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:39" class="idref" href="#t<sub>1</sub>:39"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>1</sub>':40" class="idref" href="#t<sub>1</sub>':40"><span class="id" title="binder">t<sub>1</sub>'</span></a> <a id="t<sub>2</sub>:41" class="idref" href="#t<sub>2</sub>:41"><span class="id" title="binder">t<sub>2</sub></span></a> <a id="t<sub>3</sub>:42" class="idref" href="#t<sub>3</sub>:42"><span class="id" title="binder">t<sub>3</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#t<sub>1</sub>:39"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#STLC.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>':40"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>:39"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <a class="idref" href="Stlc.html#t<sub>2</sub>:41"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <a class="idref" href="Stlc.html#t<sub>3</sub>:42"><span class="id" title="variable">t<sub>3</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#STLC.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>':40"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <a class="idref" href="Stlc.html#t<sub>2</sub>:41"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <a class="idref" href="Stlc.html#t<sub>3</sub>:42"><span class="id" title="variable">t<sub>3</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
<br/>
<span class="id" title="keyword">where</span> <a id="STLC.:::x_'--&gt;'_x" class="idref" href="#STLC.:::x_'--&gt;'_x"><span class="id" title="notation">&quot;</span></a>t '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>' t'" := (<a class="idref" href="Stlc.html#step:24"><span class="id" title="inductive">step</span></a> <span class="id" title="var">t</span> <span class="id" title="var">t'</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="Stlc.html#step"><span class="id" title="inductive">step</span></a> : <span class="id" title="var">core</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLC.multistep" class="idref" href="#STLC.multistep"><span class="id" title="abbreviation">multistep</span></a> := (<a class="idref" href="Smallstep.html#multi"><span class="id" title="inductive">multi</span></a> <a class="idref" href="Stlc.html#STLC.step"><span class="id" title="inductive">step</span></a>).<br/>
<span class="id" title="keyword">Notation</span> <a id="bec5a241f75789ab79d4eacc9e2c0fec" class="idref" href="#bec5a241f75789ab79d4eacc9e2c0fec"><span class="id" title="notation">&quot;</span></a>t<sub>1</sub> '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span>' t<sub>2</sub>" := (<a class="idref" href="Stlc.html#STLC.multistep"><span class="id" title="abbreviation">multistep</span></a> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40).<br/>
</div>

<div class="doc">
<a id="lab225"></a><h2 class="section">Examples</h2>

<div class="paragraph"> </div>

 Example:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>→<span class="id" title="var">Bool</span>, <span class="id" title="var">x</span>) (\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>, <span class="id" title="var">x</span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span> \<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>, <span class="id" title="var">x</span>
<div class="paragraph"> </div>

</span>    i.e.,
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">idBB</span> <span class="id" title="var">idB</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span> <span class="id" title="var">idB</span>
<div class="paragraph"> </div>

</span>
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLC.step_example1" class="idref" href="#STLC.step_example1"><span class="id" title="lemma">step_example1</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.idBB"><span class="id" title="abbreviation">idBB</span></a> <a class="idref" href="Stlc.html#STLC.idB"><span class="id" title="abbreviation">idB</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#bec5a241f75789ab79d4eacc9e2c0fec"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span></span></a> <a class="idref" href="Stlc.html#STLC.idB"><span class="id" title="abbreviation">idB</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Smallstep.html#multi_step"><span class="id" title="constructor">multi_step</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.ST_AppAbs"><span class="id" title="constructor">ST_AppAbs</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.v_abs"><span class="id" title="constructor">v_abs</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Smallstep.html#multi_refl"><span class="id" title="constructor">multi_refl</span></a>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Example:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>→<span class="id" title="var">Bool</span>, <span class="id" title="var">x</span>) ((\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>→<span class="id" title="var">Bool</span>, <span class="id" title="var">x</span>) (\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>, <span class="id" title="var">x</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span> \<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>, <span class="id" title="var">x</span>
<div class="paragraph"> </div>

</span>    i.e.,
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="var">idBB</span> (<span class="id" title="var">idBB</span> <span class="id" title="var">idB</span>)) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span> <span class="id" title="var">idB</span>.
<div class="paragraph"> </div>

</span>
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLC.step_example2" class="idref" href="#STLC.step_example2"><span class="id" title="lemma">step_example2</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.idBB"><span class="id" title="abbreviation">idBB</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.idBB"><span class="id" title="abbreviation">idBB</span></a> <a class="idref" href="Stlc.html#STLC.idB"><span class="id" title="abbreviation">idB</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#bec5a241f75789ab79d4eacc9e2c0fec"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span></span></a> <a class="idref" href="Stlc.html#STLC.idB"><span class="id" title="abbreviation">idB</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Smallstep.html#multi_step"><span class="id" title="constructor">multi_step</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.ST_App2"><span class="id" title="constructor">ST_App2</span></a>. <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.ST_AppAbs"><span class="id" title="constructor">ST_AppAbs</span></a>. <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Smallstep.html#multi_step"><span class="id" title="constructor">multi_step</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.ST_AppAbs"><span class="id" title="constructor">ST_AppAbs</span></a>. <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">apply</span> <a class="idref" href="Smallstep.html#multi_refl"><span class="id" title="constructor">multi_refl</span></a>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Example:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>→<span class="id" title="var">Bool</span>, <span class="id" title="var">x</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>, <span class="id" title="keyword">if</span> <span class="id" title="var">x</span> <span class="id" title="keyword">then</span> <span class="id" title="var">false</span> <span class="id" title="keyword">else</span> <span class="id" title="var">true</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">true</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span> <span class="id" title="var">false</span>
<div class="paragraph"> </div>

</span>    i.e.,
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="var">idBB</span> <span class="id" title="var">notB</span>) <span class="id" title="var">true</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span> <span class="id" title="var">false</span>.
<div class="paragraph"> </div>

</span>
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLC.step_example3" class="idref" href="#STLC.step_example3"><span class="id" title="lemma">step_example3</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.idBB"><span class="id" title="abbreviation">idBB</span></a> <a class="idref" href="Stlc.html#STLC.notB"><span class="id" title="abbreviation">notB</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#bec5a241f75789ab79d4eacc9e2c0fec"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span></span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'false'"><span class="id" title="notation">false</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Smallstep.html#multi_step"><span class="id" title="constructor">multi_step</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.ST_App1"><span class="id" title="constructor">ST_App1</span></a>. <span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.ST_AppAbs"><span class="id" title="constructor">ST_AppAbs</span></a>. <span class="id" title="tactic">auto</span>. <span class="id" title="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Smallstep.html#multi_step"><span class="id" title="constructor">multi_step</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.ST_AppAbs"><span class="id" title="constructor">ST_AppAbs</span></a>. <span class="id" title="tactic">auto</span>. <span class="id" title="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Smallstep.html#multi_step"><span class="id" title="constructor">multi_step</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.ST_IfTrue"><span class="id" title="constructor">ST_IfTrue</span></a>. <span class="id" title="tactic">apply</span> <a class="idref" href="Smallstep.html#multi_refl"><span class="id" title="constructor">multi_refl</span></a>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Example:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span> → <span class="id" title="var">Bool</span>, <span class="id" title="var">x</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;((\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>, <span class="id" title="keyword">if</span> <span class="id" title="var">x</span> <span class="id" title="keyword">then</span> <span class="id" title="var">false</span> <span class="id" title="keyword">else</span> <span class="id" title="var">true</span>) <span class="id" title="var">true</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span> <span class="id" title="var">false</span>
<div class="paragraph"> </div>

</span>    i.e.,
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">idBB</span> (<span class="id" title="var">notB</span> <span class="id" title="var">true</span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span> <span class="id" title="var">false</span>.
<div class="paragraph"> </div>

</span>    (Note that this term doesn't actually typecheck; even so, we can
    ask how it reduces.)

</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLC.step_example4" class="idref" href="#STLC.step_example4"><span class="id" title="lemma">step_example4</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.idBB"><span class="id" title="abbreviation">idBB</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.notB"><span class="id" title="abbreviation">notB</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#bec5a241f75789ab79d4eacc9e2c0fec"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span></span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'false'"><span class="id" title="notation">false</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Smallstep.html#multi_step"><span class="id" title="constructor">multi_step</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.ST_App2"><span class="id" title="constructor">ST_App2</span></a>. <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.ST_AppAbs"><span class="id" title="constructor">ST_AppAbs</span></a>. <span class="id" title="tactic">auto</span>. <span class="id" title="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Smallstep.html#multi_step"><span class="id" title="constructor">multi_step</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.ST_App2"><span class="id" title="constructor">ST_App2</span></a>. <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.ST_IfTrue"><span class="id" title="constructor">ST_IfTrue</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Smallstep.html#multi_step"><span class="id" title="constructor">multi_step</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.ST_AppAbs"><span class="id" title="constructor">ST_AppAbs</span></a>. <span class="id" title="tactic">auto</span>. <span class="id" title="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Smallstep.html#multi_refl"><span class="id" title="constructor">multi_refl</span></a>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
We can use the <span class="inlinecode"><span class="id" title="var">normalize</span></span> tactic defined in the <a href="Smallstep.html"><span class="inlineref">Smallstep</span></a> chapter
    to simplify these proofs. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLC.step_example1'" class="idref" href="#STLC.step_example1'"><span class="id" title="lemma">step_example1'</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.idBB"><span class="id" title="abbreviation">idBB</span></a> <a class="idref" href="Stlc.html#STLC.idB"><span class="id" title="abbreviation">idB</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#bec5a241f75789ab79d4eacc9e2c0fec"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span></span></a> <a class="idref" href="Stlc.html#STLC.idB"><span class="id" title="abbreviation">idB</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="var">normalize</span>. <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Lemma</span> <a id="STLC.step_example2'" class="idref" href="#STLC.step_example2'"><span class="id" title="lemma">step_example2'</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.idBB"><span class="id" title="abbreviation">idBB</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.idBB"><span class="id" title="abbreviation">idBB</span></a> <a class="idref" href="Stlc.html#STLC.idB"><span class="id" title="abbreviation">idB</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#bec5a241f75789ab79d4eacc9e2c0fec"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span></span></a> <a class="idref" href="Stlc.html#STLC.idB"><span class="id" title="abbreviation">idB</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="var">normalize</span>. <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Lemma</span> <a id="STLC.step_example3'" class="idref" href="#STLC.step_example3'"><span class="id" title="lemma">step_example3'</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.idBB"><span class="id" title="abbreviation">idBB</span></a> <a class="idref" href="Stlc.html#STLC.notB"><span class="id" title="abbreviation">notB</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#bec5a241f75789ab79d4eacc9e2c0fec"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span></span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'false'"><span class="id" title="notation">false</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="var">normalize</span>. <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Lemma</span> <a id="STLC.step_example4'" class="idref" href="#STLC.step_example4'"><span class="id" title="lemma">step_example4'</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.idBB"><span class="id" title="abbreviation">idBB</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.notB"><span class="id" title="abbreviation">notB</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Stlc.html#bec5a241f75789ab79d4eacc9e2c0fec"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span></span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'false'"><span class="id" title="notation">false</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="var">normalize</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab226"></a><h4 class="section">Exercise: 2 stars, standard (step_example5)</h4>
 Try to do this one both with and without <span class="inlinecode"><span class="id" title="var">normalize</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLC.step_example5" class="idref" href="#STLC.step_example5"><span class="id" title="lemma">step_example5</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.idBBBB"><span class="id" title="abbreviation">idBBBB</span></a> <a class="idref" href="Stlc.html#STLC.idBB"><span class="id" title="abbreviation">idBB</span></a> <a class="idref" href="Stlc.html#STLC.idB"><span class="id" title="abbreviation">idB</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#bec5a241f75789ab79d4eacc9e2c0fec"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span></span></a> <a class="idref" href="Stlc.html#STLC.idB"><span class="id" title="abbreviation">idB</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Lemma</span> <a id="STLC.step_example5_with_normalize" class="idref" href="#STLC.step_example5_with_normalize"><span class="id" title="lemma">step_example5_with_normalize</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.idBBBB"><span class="id" title="abbreviation">idBBBB</span></a> <a class="idref" href="Stlc.html#STLC.idBB"><span class="id" title="abbreviation">idBB</span></a> <a class="idref" href="Stlc.html#STLC.idB"><span class="id" title="abbreviation">idB</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#bec5a241f75789ab79d4eacc9e2c0fec"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span></span></a> <a class="idref" href="Stlc.html#STLC.idB"><span class="id" title="abbreviation">idB</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab227"></a><h1 class="section">Typing</h1>

<div class="paragraph"> </div>

 Next we consider the typing relation of the STLC. 
</div>

<div class="doc">
<a id="lab228"></a><h2 class="section">Contexts</h2>

<div class="paragraph"> </div>

 <i>Question</i>: What is the type of the term "<span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span>"?

<div class="paragraph"> </div>

    <i>Answer</i>: It depends on the types of <span class="inlinecode"><span class="id" title="var">x</span></span> and <span class="inlinecode"><span class="id" title="var">y</span></span>!

<div class="paragraph"> </div>

    I.e., in order to assign a type to a term, we need to know
    what assumptions we should make about the types of its free
    variables.

<div class="paragraph"> </div>

    This leads us to a three-place <i>typing judgment</i>, informally
    written <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>, where <span class="inlinecode"><span class="id" title="var">Gamma</span></span> is a
    "typing context" -- a mapping from variables to their types. 
<div class="paragraph"> </div>

 Following the usual notation for partial maps, we write <span class="inlinecode">(<span class="id" title="var">X</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span>
    <span class="inlinecode"><span class="id" title="var">T</span>,</span> <span class="inlinecode"><span class="id" title="var">Gamma</span>)</span> for "update the partial function <span class="inlinecode"><span class="id" title="var">Gamma</span></span> so that it
    maps <span class="inlinecode"><span class="id" title="var">x</span></span> to <span class="inlinecode"><span class="id" title="var">T</span></span>." 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Definition</span> <a id="STLC.context" class="idref" href="#STLC.context"><span class="id" title="definition">context</span></a> := <span class="id" title="definition">partial_map</span> <a class="idref" href="Stlc.html#STLC.ty"><span class="id" title="inductive">ty</span></a>.<br/>
</div>

<div class="doc">
<a id="lab229"></a><h2 class="section">Typing Relation</h2>

<div class="paragraph"> </div>

 <center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">Gamma x = T<sub>1</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (T_Var) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; x &#x2208; T<sub>1</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">x <span class="nowrap"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> T<sub>2</sub> ; Gamma &#x22A2; t<sub>1</sub> &#x2208; T<sub>1</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (T_Abs) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; \x:T<sub>2</sub>,t<sub>1</sub> &#x2208; T<sub>2</sub><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>T<sub>1</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; t<sub>1</sub> &#x2208; T<sub>2</sub><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>T<sub>1</sub></td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; t<sub>2</sub> &#x2208; T<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (T_App) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; t<sub>1</sub> t<sub>2</sub> &#x2208; T<sub>1</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (T_True) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; true &#x2208; Bool</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (T_False) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; false &#x2208; Bool</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; t<sub>1</sub> &#x2208; Bool&nbsp;&nbsp;&nbsp;&nbsp;Gamma &#x22A2; t<sub>2</sub> &#x2208; T<sub>1</sub>&nbsp;&nbsp;&nbsp;&nbsp;Gamma &#x22A2; t<sub>3</sub> &#x2208; T<sub>1</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (T_If) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; if t<sub>1</sub> then t<sub>2</sub> else t<sub>3</sub> &#x2208; T<sub>1</sub></td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

    We can read the three-place relation <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> as:
    "under the assumptions in Gamma, the term <span class="inlinecode"><span class="id" title="var">t</span></span> has the type <span class="inlinecode"><span class="id" title="var">T</span></span>." 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Reserved Notation</span> &quot;Gamma '&#x22A2;' t '&#x2208;' T" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 101,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">t</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span>, <span class="id" title="var">T</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Inductive</span> <a id="STLC.has_type" class="idref" href="#STLC.has_type"><span class="id" title="inductive">has_type</span></a> : <a class="idref" href="Stlc.html#STLC.context"><span class="id" title="definition">context</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#STLC.ty"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="STLC.T_Var" class="idref" href="#STLC.T_Var"><span class="id" title="constructor">T_Var</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:45" class="idref" href="#Gamma:45"><span class="id" title="binder">Gamma</span></a> <a id="x:46" class="idref" href="#x:46"><span class="id" title="binder">x</span></a> <a id="T<sub>1</sub>:47" class="idref" href="#T<sub>1</sub>:47"><span class="id" title="binder">T<sub>1</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#Gamma:45"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#x:46"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Stlc.html#T<sub>1</sub>:47"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#Gamma:45"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#x:46"><span class="id" title="variable">x</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#T<sub>1</sub>:47"><span class="id" title="variable">T<sub>1</sub></span></a><br/>
&nbsp;&nbsp;| <a id="STLC.T_Abs" class="idref" href="#STLC.T_Abs"><span class="id" title="constructor">T_Abs</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:48" class="idref" href="#Gamma:48"><span class="id" title="binder">Gamma</span></a> <a id="x:49" class="idref" href="#x:49"><span class="id" title="binder">x</span></a> <a id="T<sub>1</sub>:50" class="idref" href="#T<sub>1</sub>:50"><span class="id" title="binder">T<sub>1</sub></span></a> <a id="T<sub>2</sub>:51" class="idref" href="#T<sub>2</sub>:51"><span class="id" title="binder">T<sub>2</sub></span></a> <a id="t<sub>1</sub>:52" class="idref" href="#t<sub>1</sub>:52"><span class="id" title="binder">t<sub>1</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#x:49"><span class="id" title="variable">x</span></a> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <a class="idref" href="Stlc.html#T<sub>2</sub>:51"><span class="id" title="variable">T<sub>2</sub></span></a> <span class="id" title="notation">;</span> <a class="idref" href="Stlc.html#Gamma:48"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>:52"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#T<sub>1</sub>:50"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#Gamma:48"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#x:49"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#T<sub>2</sub>:51"><span class="id" title="variable">T<sub>2</sub></span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>:52"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#T<sub>2</sub>:51"><span class="id" title="variable">T<sub>2</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#T<sub>1</sub>:50"><span class="id" title="variable">T<sub>1</sub></span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.T_App" class="idref" href="#STLC.T_App"><span class="id" title="constructor">T_App</span></a> : <span class="id" title="keyword">∀</span> <a id="T<sub>1</sub>:53" class="idref" href="#T<sub>1</sub>:53"><span class="id" title="binder">T<sub>1</sub></span></a> <a id="T<sub>2</sub>:54" class="idref" href="#T<sub>2</sub>:54"><span class="id" title="binder">T<sub>2</sub></span></a> <a id="Gamma:55" class="idref" href="#Gamma:55"><span class="id" title="binder">Gamma</span></a> <a id="t<sub>1</sub>:56" class="idref" href="#t<sub>1</sub>:56"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:57" class="idref" href="#t<sub>2</sub>:57"><span class="id" title="binder">t<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#Gamma:55"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>:56"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#T<sub>2</sub>:54"><span class="id" title="variable">T<sub>2</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#T<sub>1</sub>:53"><span class="id" title="variable">T<sub>1</sub></span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#Gamma:55"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#t<sub>2</sub>:57"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#T<sub>2</sub>:54"><span class="id" title="variable">T<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#Gamma:55"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>:56"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#t<sub>2</sub>:57"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#T<sub>1</sub>:53"><span class="id" title="variable">T<sub>1</sub></span></a><br/>
&nbsp;&nbsp;| <a id="STLC.T_True" class="idref" href="#STLC.T_True"><span class="id" title="constructor">T_True</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:58" class="idref" href="#Gamma:58"><span class="id" title="binder">Gamma</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#Gamma:58"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.T_False" class="idref" href="#STLC.T_False"><span class="id" title="constructor">T_False</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:59" class="idref" href="#Gamma:59"><span class="id" title="binder">Gamma</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#Gamma:59"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'false'"><span class="id" title="notation">false</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><br/>
&nbsp;&nbsp;| <a id="STLC.T_If" class="idref" href="#STLC.T_If"><span class="id" title="constructor">T_If</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:60" class="idref" href="#t<sub>1</sub>:60"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:61" class="idref" href="#t<sub>2</sub>:61"><span class="id" title="binder">t<sub>2</sub></span></a> <a id="t<sub>3</sub>:62" class="idref" href="#t<sub>3</sub>:62"><span class="id" title="binder">t<sub>3</sub></span></a> <a id="T<sub>1</sub>:63" class="idref" href="#T<sub>1</sub>:63"><span class="id" title="binder">T<sub>1</sub></span></a> <a id="Gamma:64" class="idref" href="#Gamma:64"><span class="id" title="binder">Gamma</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#Gamma:64"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>:60"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#Gamma:64"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#t<sub>2</sub>:61"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#T<sub>1</sub>:63"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#Gamma:64"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#t<sub>3</sub>:62"><span class="id" title="variable">t<sub>3</sub></span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#T<sub>1</sub>:63"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#Gamma:64"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <a class="idref" href="Stlc.html#t<sub>1</sub>:60"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <a class="idref" href="Stlc.html#t<sub>2</sub>:61"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <a class="idref" href="Stlc.html#t<sub>3</sub>:62"><span class="id" title="variable">t<sub>3</sub></span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#T<sub>1</sub>:63"><span class="id" title="variable">T<sub>1</sub></span></a><br/>
<br/>
<span class="id" title="keyword">where</span> <a id="092ca644792e367ec17fc46e3cfd4c<sub>33</sub>" class="idref" href="#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&quot;</span></a>Gamma '&#x22A2;' t '&#x2208;' T" := (<a class="idref" href="Stlc.html#has_type:44"><span class="id" title="inductive">has_type</span></a> <span class="id" title="var">Gamma</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="Stlc.html#has_type"><span class="id" title="inductive">has_type</span></a> : <span class="id" title="var">core</span>.<br/>
</div>

<div class="doc">
<a id="lab230"></a><h2 class="section">Examples</h2>

</div>
<div class="code">

<br/>
<span class="id" title="keyword">Example</span> <a id="STLC.typing_example_1" class="idref" href="#STLC.typing_example_1"><span class="id" title="definition">typing_example_1</span></a> :<br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.T_Abs"><span class="id" title="constructor">T_Abs</span></a>. <span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.T_Var"><span class="id" title="constructor">T_Var</span></a>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Note that, since we added the <span class="inlinecode"><span class="id" title="var">has_type</span></span> constructors to the hints
    database, <span class="inlinecode"><span class="id" title="tactic">auto</span></span> can actually solve this one immediately. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Example</span> <a id="STLC.typing_example_1'" class="idref" href="#STLC.typing_example_1'"><span class="id" title="definition">typing_example_1'</span></a> :<br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">auto</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
More examples:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">empty</span> &#x22A2; \<span class="id" title="var">x</span>:<span class="id" title="var">A</span>, \<span class="id" title="var">y</span>:<span class="id" title="var">A</span>→<span class="id" title="var">A</span>, <span class="id" title="var">y</span> (<span class="id" title="var">y</span> <span class="id" title="var">x</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\<span class="id" title="tactic">in</span> <span class="id" title="var">A</span> → (<span class="id" title="var">A</span>→<span class="id" title="var">A</span>) → <span class="id" title="var">A</span>.
<div class="paragraph"> </div>

</span>
</div>
<div class="code">
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">

<br/>
<span class="id" title="keyword">Example</span> <a id="STLC.typing_example_2" class="idref" href="#STLC.typing_example_2"><span class="id" title="definition">typing_example_2</span></a> :<br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a> <a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">))</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.T_Abs"><span class="id" title="constructor">T_Abs</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.T_Abs"><span class="id" title="constructor">T_Abs</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Stlc.html#STLC.T_App"><span class="id" title="constructor">T_App</span></a>. <span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.T_Var"><span class="id" title="constructor">T_Var</span></a>. <span class="id" title="tactic">apply</span> <span class="id" title="lemma">update_eq</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Stlc.html#STLC.T_App"><span class="id" title="constructor">T_App</span></a>. <span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.T_Var"><span class="id" title="constructor">T_Var</span></a>. <span class="id" title="tactic">apply</span> <span class="id" title="lemma">update_eq</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Stlc.html#STLC.T_Var"><span class="id" title="constructor">T_Var</span></a>. <span class="id" title="tactic">apply</span> <span class="id" title="lemma">update_neq</span>. <span class="id" title="tactic">intros</span> <span class="id" title="var">Contra</span>. <span class="id" title="tactic">discriminate</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab231"></a><h4 class="section">Exercise: 2 stars, standard, optional (typing_example_2_full)</h4>
 Prove the same result without using <span class="inlinecode"><span class="id" title="tactic">auto</span></span>, <span class="inlinecode"><span class="id" title="tactic">eauto</span></span>, or
    <span class="inlinecode"><span class="id" title="tactic">eapply</span></span> (or <span class="inlinecode">...</span>). 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Example</span> <a id="STLC.typing_example_2_full" class="idref" href="#STLC.typing_example_2_full"><span class="id" title="definition">typing_example_2_full</span></a> :<br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a> <a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">))</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab232"></a><h4 class="section">Exercise: 2 stars, standard (typing_example_3)</h4>
 Formally prove the following typing derivation holds:  <br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">empty</span> &#x22A2; \<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>→<span class="id" title="var">B</span>, \<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>→<span class="id" title="var">Bool</span>, \<span class="id" title="var">z</span>:<span class="id" title="var">Bool</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">y</span> (<span class="id" title="var">x</span> <span class="id" title="var">z</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\<span class="id" title="tactic">in</span> <span class="id" title="var">T</span>.
<div class="paragraph"> </div>

</span>
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Example</span> <a id="STLC.typing_example_3" class="idref" href="#STLC.typing_example_3"><span class="id" title="definition">typing_example_3</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="T:65" class="idref" href="#T:65"><span class="id" title="binder">T</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.z"><span class="id" title="definition">z</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a> <a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a> <a class="idref" href="Stlc.html#STLC.z"><span class="id" title="definition">z</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">))</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#T:65"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 We can also show that some terms are <i>not</i> typable.  For example,
    let's check that there is no typing derivation assigning a type
    to the term <span class="inlinecode">\<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode">\<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>,</span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span> -- i.e.,
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;¬<span class="id" title="tactic">∃</span> <span class="id" title="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">empty</span> &#x22A2; \<span class="id" title="var">x</span>:<span class="id" title="var">Bool</span>, \<span class="id" title="var">y</span>:<span class="id" title="var">Bool</span>, <span class="id" title="var">x</span> <span class="id" title="var">y</span> \<span class="id" title="tactic">in</span> <span class="id" title="var">T</span>.
<div class="paragraph"> </div>

</span>
</div>
<div class="code">
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">

<br/>
<span class="id" title="keyword">Example</span> <a id="STLC.typing_nonexample_1" class="idref" href="#STLC.typing_nonexample_1"><span class="id" title="definition">typing_nonexample_1</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">¬</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="T:66" class="idref" href="#T:66"><span class="id" title="binder">T</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a> <a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#T:66"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Hc</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">Hc</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">T</span> <span class="id" title="var">Hc</span>].<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;<span class="inlinecode"><span class="id" title="tactic">clear</span></span>&nbsp;tactic&nbsp;is&nbsp;useful&nbsp;here&nbsp;for&nbsp;tidying&nbsp;away&nbsp;bits&nbsp;of<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;the&nbsp;context&nbsp;that&nbsp;we're&nbsp;not&nbsp;going&nbsp;to&nbsp;need&nbsp;again.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">Hc</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">Hc</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>4</sub></span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">H<sub>4</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>5</sub></span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">H<sub>5</sub></span> <span class="id" title="var">H<sub>4</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>2</sub></span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">discriminate</span> <span class="id" title="var">H<sub>1</sub></span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab233"></a><h4 class="section">Exercise: 3 stars, standard, optional (typing_nonexample_3)</h4>
 Another nonexample:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;¬(<span class="id" title="tactic">∃</span> <span class="id" title="var">S</span> <span class="id" title="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">empty</span> &#x22A2; \<span class="id" title="var">x</span>:<span class="id" title="var">S</span>, <span class="id" title="var">x</span> <span class="id" title="var">x</span> \<span class="id" title="tactic">in</span> <span class="id" title="var">T</span>).
<div class="paragraph"> </div>

</span>
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Example</span> <a id="STLC.typing_nonexample_3" class="idref" href="#STLC.typing_nonexample_3"><span class="id" title="definition">typing_nonexample_3</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">¬</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="S:67" class="idref" href="#S:67"><span class="id" title="binder">S</span></a> <a id="T:68" class="idref" href="#T:68"><span class="id" title="binder">T</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#S:67"><span class="id" title="variable">S</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a> <a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Stlc.html#T:68"><span class="id" title="variable">T</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="code">

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Stlc.html#STLC"><span class="id" title="module">STLC</span></a>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;2020-08-24&nbsp;16:13&nbsp;*)</span><br/>
</div>
</div>

<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>

</div>

</body>
</html>